#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <sys/time.h>
#include <unistd.h>
#include <pthread.h>
#include <Judy.h>

#include "model/globals.h"
#include "model/initialization.h"
#include "model/print_utils.h"
#include "normalization/normalization.h"
#include "normalization/normalization_globals.h"
#include "normalization/print_utils.h"
#include "preprocessing/preprocessing.h"
#include "completion/completion.h"
#include "completion/print_utils.h"

extern int yyparse(void);
extern FILE *yyin;

struct timeval tStart, tEnd;
#define START_TIMER	gettimeofday(&tStart, NULL)
#define STOP_TIMER	gettimeofday(&tEnd, NULL)
#define TIME_DIFF	(((double)tEnd.tv_sec * 1000000.0 + \
	(double)tEnd.tv_usec) - \
	((double)tStart.tv_sec * 1000000.0 + (double)tStart.tv_usec) )


int main(int argc, char *argv[]) {
	int parser;

	if (argc <= 1) {
		fprintf(stderr,"syntax: %s filename\n", argv[0]);
		return -1;
	}

	yyin = fopen(argv[1], "r");

	printf("Initializing ELC...");
	init();
	printf("\tdone\n");

	printf("Loading KB...");
	fflush(stdout);
	START_TIMER;
	parser = yyparse();
	STOP_TIMER;
	if (parser != 0) {	
		print_short_stats();
		fprintf(stderr,"aborting\n");
		exit(-1);
	}
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);
	print_short_stats();
	// printf("-------EquivalentClass Axioms---------\n");
	// print_eqclass_axioms();
	// printf("-------SubClass Axioms---------\n");
	// print_subclass_axioms();
	// printf("------- Axioms---------\n");
	// print_axioms(tbox.axioms,tbox.axiom_count);

	// printf("Normalizing KB on %d core(s)...",core_count);
	printf("Normalizing KB ...");
	fflush(stdout);
	START_TIMER;
	normalize_tbox(tbox,&normalized_tbox);
	STOP_TIMER;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);
	print_normalization_stats();
	// printf("------- Normalized Axioms---------\n");
	// print_normalized_axioms(normalized_tbox.axioms,normalized_tbox.axiom_count);
	// print_normalized_tbox();
	// realloc space for original axioms and normalized axioms
	// for shrinking the dynamic arrays to the actual number of original
	// and normalized axioms
	reInit();

	printf("Preprocessing the normalized KB ...");
	START_TIMER;
	preprocess();
	STOP_TIMER;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);

	printf("Completing the normalized KB ...");
	START_TIMER;
	complete_kb();
	STOP_TIMER;
	printf("\tdone in %.3f milisecs\n", TIME_DIFF / 1000);

	// print_subsumer_lists();
	getchar();

	return 0;
}

